A:Type, f:(A(A + Top)), x:A, m, n:.
(can-apply(f^m;x))  ((f^n+m(x)) ~ (f^n(do-apply(f^m;x)))) 

latex

ProofTree

Definitions	Void, t  T, x:A.B(x), Top, x:AB(x), x:A. B(x), S  T, left + right, A  B, #$n, a < b, P  Q, False, A, {x:A| B(x)} , , suptype(S; T), f^n, can-apply(f;x), b, , s ~ t, Type, i  j , -n, n+m, n - m, p-id(), do-apply(f;x), {T}, SQType(T), s = t, , P  Q, Dec(P), f(a), f o g  , primrec(n;b;c), x.A(x), b, , (i = j), x:A  B(x), P & Q, P  Q, Unit, if b then t else f fi , outl(x), True, T, isl(x)
Lemmas	nat sq, p-compose wf, bool sq, isl wf, p-fun-exp-add1-sq, can-apply-fun-exp, bool wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, bnot wf, not wf, inl-do-apply, decidable int equal, ge wf, nat properties, nat wf, assert wf, can-apply wf, p-fun-exp wf, le wf, top wf